Section: New Results

Formal Verification of Transformations on Data Dependency in Synchronous Compilers

Participants : Van-Chan Ngo, Jean-Pierre Talpin, Paul Le Guernic.

We propose an approach to prove the data dependency semantic preservation of transformations in a synchronous compiler (such as that of Signal). In the Signal language, the scheduling or data dependency is expressed implicitly through polychronous equations. We use Synchronous Data-flow Dependence Graphs (SDD Graphs) [46] , [50] to formalize the data dependency semantics of polychronous equations. A tuple $<G,C,fE>$ is a SDD graph if and only if:

• $G=<N,E,I,O>$ is a dependence graph $<N,E>$ with I/O nodes: the inputs $I$ and the output $O$ such that $I$, $O$ are subsets of $N$ and $I$ and $O$ are disjoint.

• $C$ is a set of constraints, called clocks.

• $fE:E⟶C$ is a mapping labeling each edge with a clock; it specifies the existence condition of the edges.

For instance, for the counter example:

$zv:=v\$1|v:=(1\text{when}rst)\text{default}zv+1$

we get a SDD graph with:

• $N=\{1,v,zv+1\}$

• $E=\left\{\right(1,v),(zv+1,v\left)\right\}$

• $C=\{\widehat{rst},\widehat{v}\wedge \neg \widehat{rst}\}$

• $fE\left((1,v)\right)=\widehat{rst},fE\left((zv+1,v)\right)=\widehat{v}\wedge \neg \widehat{rst}$

Let $SD{D}_1=<G_1,C_1,f{E}_1>$ and $SD{D}_2=<G_2,C_2,f{E}_2>$ to be two SDD graphs which represent the data dependency semantics of source and transformed programs, we say that $SD{D}_2$ is a correct transformation of $SD{D}_1$ on data dependency, or $SD{D}_2$ refines $SD{D}_1$ w.r.t the data dependency semantics, if it satisfies that for any pair of nodes $x,y\in G_1\cap G_2$ with $(x,y)\in E_1$:

• $f{E}_1(x,y))\Rightarrow ((x,y)\in E_2\wedge f{E}_2(x,y))$ (reinforcement)

• $(f{E}_2(x,y)\wedge f{E}_2(y,x)\iff \text{false})$ (deadlock consistency)